<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html; charset=ISO-8859-1"
 http-equiv="content-type">
  <title>ProofAssistantGUIQuickHOWTO</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
 alink="#000088" link="#0000ff" vlink="#ff0000">
<big><big><span style="font-weight: bold;">Proof Assistant GUI Detailed
Info<br>
<br>
</span></big></big>back to <a href="ProofAssistantGUIQuickHOWTO.html">ProofAssistantGUIQuickHOWTO.html</a><br>
forward to <a href="ProofAssistantGUIDeriveFeature.html">ProofAssistantGUIDeriveFeature.html</a><br>
<br>
see also:<br>
<a href="PAUserGuide/Start.html">Proof Assistant User Guide</a><br>
<a href="StepUnifier.html">StepUnifier.html</a><br>
<a href="WorkVariables.html">WorkVariables.html</a><br>
<a href="../mmj2jar/PATutorial/PageLocalRef.mmp">PageLocalRef.mmp</a><br>
<a href="StepSelectorSearch.html">StepSelectorSearch.html</a><br>
<a href="UnifyEraseAndRederiveFormulasFeature.html">UnifyEraseAndRederiveFormulas.html</a><br>
<a href="BottomUpProving-ByNormMegill.html">BottomUpProving-ByNormMegill.html</a><br>
<big><big><span style="font-weight: bold;">
</span></big></big>
<hr style="width: 100%; height: 2px;"><br>
<big><span style="font-weight: bold;"><big>Proof Text Area Statement
Types:</big><br>
</span></big>
<ul>
  <li><a href="#HEADER_STATEMENT_TYPE"><big><span
 style="font-weight: bold;">Header</span></big></a></li>
  <li><a href="#PROOF_STEP_STATEMENT_TYPE"><big><span
 style="font-weight: bold;">Proof Step</span></big></a></li>
  <li><a href="#COMMENT_STATEMENT_TYPE"><big><span
 style="font-weight: bold;">Comment</span></big></a></li>
  <li><a href="#DISTINCT_VARIABLE_STATEMENT_TYPE"><big><span
 style="font-weight: bold;">Distinct Variable</span></big></a></li>
  <li><a href="#FOOTER_STATEMENT_TYPE"><big><span
 style="font-weight: bold;">Footer</span></big></a></li>
  <li><big><span style="font-weight: bold;"><a
 href="#GENERATED_PROOF_STATEMENT_TYPE">Generated Proof</a><br>
    </span></big></li>
</ul>
<br>
<hr style="width: 100%; height: 2px;"><big><big><span
 style="font-weight: bold;"><a name="HEADER_STATEMENT_TYPE"></a>HEADER
Statement Type</span></big></big><br>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Header:</span><br>
      <ul>
        <li>Mandatory.<br>
        </li>
        <li>Identified by a "<code style="font-weight: bold;">$(</code>"
token in column 1 of the first line of the Proof Text area (by "token"
we mean that whitespace follows the "<code style="font-weight: bold;">$(</code>"
characters), followed by the&nbsp;<big><span
 style="font-family: monospace; font-weight: bold;"> </span></big>"<big><span
 style="font-family: monospace; font-weight: bold;">&lt;MM&gt;</span></big>"
and<big><span style="font-family: monospace; font-weight: bold;"> </span></big>"<big><span
 style="font-family: monospace; font-weight: bold;">&lt;PROOF_ASST&gt;</span></big>"&nbsp;&nbsp;
tokens. </li>
        <li>Contains the keyword parameter fields <code
 style="font-weight: bold;">THEOREM=</code> <span
 style="text-decoration: underline;">followed by</span> <code
 style="font-weight: bold;">LOC_AFTER=</code>&nbsp;</li>
        <li>Any tokens following the <code style="font-weight: bold;">LOC_AFTER=</code>
value and prior to the start of the next Proof Assistant Statement (<span
 style="font-weight: bold;">Comment</span>, <span
 style="font-weight: bold;">Proof Step</span>, <span
 style="font-weight: bold;">Distinct Variable</span> or <span
 style="font-weight: bold;">Footer</span>)
are absolutely forbidden :)</li>
      </ul>
      <br>
      </td>
    </tr>
  </tbody>
</table>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Header
Fields</span><br>
      </td>
      <td style="vertical-align: top;">================================================<br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><code style="font-weight: bold;">THEOREM=</code><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Mandatory</li>
        <li>Specifies the Label of a Theorem in the loaded Metamath
.mm database, or a Label that does not exist in the Metamath .mm
database.</li>
        <li>If the <code style="font-weight: bold;">THEOREM</code>
Label already exists in the database, then it must designate a Metamath
Theorem, and the Type Code of the Theorem must match the Grammar's
Provable Logic Statement Type (default is "<code
 style="font-weight: bold;">|-</code>" -- Proof Assistant does not <span
 style="font-style: italic;">do</span> syntax proofs :)<br>
        </li>
        <li>Otherwise, if the <code style="font-weight: bold;">THEOREM</code>
Label does not exist in the loaded Metamath .mm database, then the
Proof Text area will first be used to build a temporary theorem in
memory, after which the Proof Text is validated/unified.<br>
        </li>
      </ul>
      <br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><code style="font-weight: bold;">LOC_AFTER=</code><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Optional</li>
        <li>Follows the <code style="font-weight: bold;">THEOREM=</code>&nbsp;
parameter value<br>
        </li>
        <li>Used only if the <code style="font-weight: bold;">THEOREM=</code>
Label does not already exist in the loaded Metamath .mm database;
otherwise it is ignored.<br>
        </li>
        <li>Can specify any Label in the Metamath database (Metamath
statements that have Labels are the $e, $f, $p and $a statements -- the
hypotheses and assertions.) <br>
        </li>
        <li>If the specified Label does not exist, an
error message is displayed and validation/unification processing is
halted.<br>
        </li>
        <li><span style="text-decoration: underline;">If left blank or
equal to "</span><code
 style="font-weight: bold; text-decoration: underline;">?</code><span
 style="text-decoration: underline;">"
for a new Theorem</span> (<code style="font-weight: bold;">THEOREM=</code>
not in the database), <span style="text-decoration: underline;">then
the logical location of
the new Theorem for parsing/validation/unification purposes is the end
of the database</span> (recall that a Metamath statement can only refer
to
statements defined earlier in the .mm database/file.)</li>
      </ul>
      <br>
      </td>
    </tr>
  </tbody>
</table>
<br>
<br>
<br>
<br>
<br>
<hr style="width: 100%; height: 2px;"><br>
<big><big><span style="font-weight: bold;"><a
 name="PROOF_STEP_STATEMENT_TYPE"></a>PROOF STEP Statement Type</span></big></big><br>
<big><span style="font-weight: bold;"></span></big><br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Proof
Step</span>: <br>
      <ul>
        <li>Mandatory that at least one Proof Step be present -- the "<code
 style="font-weight: bold;">qed</code>" step.<br>
        </li>
        <li>A proof step consists of <span style="font-weight: bold;">Step:Hyp:Ref</span>
fields combined into one token (no intervening space characters),
followed by a <span style="font-weight: bold;">Formula</span>.</li>
        <li>There are two types of Proof Steps: <span
 style="font-style: italic;">Hypothesis Steps</span> and <span
 style="font-style: italic;">Derivation Steps</span>.<br>
        </li>
        <li>Hypothesis Proof Steps are denoted with 'h' prefixing <span
 style="font-weight: bold;">Step</span> in <span
 style="font-weight: bold;">Step:Hyp:Ref</span> and<span
 style="font-weight: bold;"> </span>correspond to the theorem's
Logical Hypotheses.<span style="font-weight: bold;"><br>
          </span></li>
        <li>Derivation Proof Steps are denoted by the absence of an 'h'
prefixing Step in <span style="font-weight: bold;">Step</span> in <span
 style="font-weight: bold;">Step:Hyp:Ref.</span></li>
      </ul>
Example stating that Proof Step #<code style="font-weight: bold;">3</code>,
using Proof Steps #<code style="font-weight: bold;">1</code> and <code
 style="font-weight: bold;">2</code> as hypotheses, justified by&nbsp;
statement label <code style="font-weight: bold;">ax-mp</code> validly
derives the Formula "<code style="font-weight: bold;">|- ( ps -&gt; ph )</code>":<br>
      <ul>
        <li><code style="font-weight: bold;">3:1,2:ax-mp |- ( ps -&gt;
ph )</code></li>
      </ul>
The user could also input this, leaving off the <span
 style="font-weight: bold;">Ref</span> field which is generated by the
Proof Assistant:<br>
      <ul>
        <li><code style="font-weight: bold;">3:1,2 &nbsp; &nbsp; &nbsp;
|- ( ps -&gt; ph )</code></li>
      </ul>
Or,
if the hypotheses for the step are unknown or not yet input, the
following can be input signifying that the step is incomplete (but can
be used for unification of subsequent steps):<br>
      <ul>
        <li><code style="font-weight: bold;">3:?,? &nbsp; &nbsp; &nbsp;
|- ( ps -&gt; ph )</code></li>
      </ul>
Or, using the "Derive" feature, the user can input <span
 style="font-weight: bold;">Ref</span> along with and omit one or both <span
 style="font-weight: bold;">Hyp</span>s (or signify a missing <code
 style="font-weight: bold;"></code><span style="font-weight: bold;">Hyp</span>
using "?"), and/or omit the <span style="font-weight: bold;">Formula</span>,
like
this:<br>
      <ul>
        <li><code style="font-weight: bold;">3:?:ax-mp</code></li>
      </ul>
Or this:<br>
      <ul>
        <li><code style="font-weight: bold;">3::ax-mp</code></li>
      </ul>
Or this:<br>
      <ul>
        <li><code style="font-weight: bold;">3:1,?:ax-mp</code></li>
      </ul>
The sequence of Proof Steps is arbitrary (need not be in final Metamath
order), except that:<br>
      <ul>
        <li>the final Proof Step must be the "qed" step,&nbsp; the
conclusion or thing-to-be-proved step; and</li>
        <li>the Hyp's for a given Proof Step may only refer to
previously entered Proof Steps in the Proof Text area -- or '<code
 style="font-weight: bold;">?</code>'.<br>
        </li>
      </ul>
      <br>
      </td>
    </tr>
  </tbody>
</table>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Proof
Step Fields</span><br>
      </td>
      <td style="vertical-align: top;">===============================================<br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Step:Hyp:Ref</span><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Mandatory</li>
        <li>Must begin in column 1 of a proof text area line<br>
        </li>
        <li>Must be a single token -- i.e. no embedded whitespace
characters<br>
        </li>
        <li>Colon ("<code style="font-weight: bold;">:</code>")
characters are used to separate the <span style="font-weight: bold;">Step</span>,
          <span style="font-weight: bold;">Hyp</span> and <span
 style="font-weight: bold;">Ref</span> sub-fields, but can be omitted
if no remaining sub-fields are needed.</li>
        <li>Example: "<code style="font-weight: bold;">h1</code>" could
be a valid <span style="font-weight: bold;">Step</span><code
 style="font-weight: bold;">:</code><span style="font-weight: bold;">Hyp</span><code
 style="font-weight: bold;">:</code><span style="font-weight: bold;">Ref</span>
entry because a hypothesis should not refer to other hypotheses, and
the Proof Assistant outputs <span style="font-weight: bold;">Ref</span>
as part of Unification!</li>
      </ul>
      <br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Step</span><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Mandatory</li>
        <li>Must be a positive integer except for the last step
"number", which must equal "<code><span style="font-weight: bold;">qed</span></code>"</li>
        <li>Prefix with "<code style="font-weight: bold;">h</code>" to
indicate that the step's <span style="font-weight: bold;">Formula</span>
is one of the theorem's hypotheses (the "<code
 style="font-weight: bold;">h</code>" is not used in subsequent Proof
Step Hyp fields.)<br>
        </li>
        <li>Need not be assigned in numeric order (numbers are being
used to maintain semantic cohesiveness, not for doing arithmetic.)<br>
        </li>
        <li>Must not duplicate the <span style="font-weight: bold;">Step</span>
number of any other Proof Step</li>
        <li>Terminate the <span style="font-weight: bold;">Step</span>
field with a Colon ("<code style="font-weight: bold;">:</code>") if the
          <span style="font-weight: bold;">Step</span> field is to be
followed by <span style="font-weight: bold;">Hyp</span> and/or <span
 style="font-weight: bold;">Ref</span> fields.</li>
      </ul>
      <br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Hyp</span><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Optional (depending on the Ref assertion's hypotheses).<br>
        </li>
        <li>Specifies the hypotheses
needed by the theorem or axiom used to derive the Proof Step's <span
 style="font-weight: bold;">Formula.</span></li>
        <li>The
number of hypotheses input controls the Unification search: if 2
hypotheses are input and Ref is blank (to be computed), then only
assertions with 2 Logical Hypotheses are searched during Unification.</li>
        <li>If present, <span style="font-weight: bold;">Hyp</span>
must be a sequence of positive integers&nbsp; or "<code
 style="font-weight: bold;">?</code>"s separated by Comma ("<code
 style="font-weight: bold;">,</code>") characters with no embedded
whitespace characters.<br>
        </li>
        <li><span style="text-decoration: underline;">Do not prefix with</span>
"<code><span style="font-weight: bold;">h</span></code>" <span
 style="text-decoration: underline;">when referring to previous Step
that is one of the theorem's hypotheses</span>.<br>
        </li>
        <li>Example of multiple <span style="font-weight: bold;">Hyp</span>'s
in <span style="font-weight: bold;">Step<code>:</code>Hyp<code>:</code>Ref</span>:
"<code><span style="font-weight: bold;">3:1,2:ax-mp</span></code>"<span
 style="font-weight: bold;"></span><br>
        </li>
        <li>Code as null, not as space character(s) if unused (the <code
 style="font-weight: bold;">Ref</code> theorem or axiom uses no
hypotheses.)<br>
        </li>
        <li>Example of omitted Hyp field in <span
 style="font-weight: bold;">Step<code>:</code>Hyp<code>:</code>Ref</span>:
"<code><span style="font-weight: bold;">5::ax-1</span></code>" (ax-1
requires no hypotheses).<br>
        </li>
        <li>Should not be input on a hypothesis Proof Step
(that is illogical, it does not compute -- an hypothesis does not have
hypotheses! :)</li>
        <li>Terminate the <span style="font-weight: bold;">Hyp</span>
field with a Colon ("<code style="font-weight: bold;">:</code>") if the
          <span style="font-weight: bold;">Hyp</span> field is to be
followed by a <span style="font-weight: bold;">Ref</span> field.</li>
        <li>Note: <span
 style="font-weight: bold; text-decoration: underline;">Hyp</span><span
 style="text-decoration: underline;"> numbers
will be resequenced by Proof Assistant during Unification to match the
Metamath sequence of the hypotheses for the theorem or axiom</span>.
For example, if Theorem <code><span style="font-weight: bold;">XYZ</span></code>
has Hypotheses <code style="font-weight: bold;">XYZ.1</code> and <code
 style="font-weight: bold;">XYZ.2</code> and the user specifies the <span
 style="font-weight: bold;">Hyp</span> as "<code
 style="font-weight: bold;">3,4</code>", but the Proof Assistant
determines that step <code><span style="font-weight: bold;">4</span></code>
corresponds to <code style="font-weight: bold;">XYZ.1</code> and step <code
 style="font-weight: bold;">3</code> corresponds to <code
 style="font-weight: bold;">XYZ.2</code>, then, when the proof text is
redisplayed after unification, the <span style="font-weight: bold;">Hyp</span>
field will be shown as "<code><span style="font-weight: bold;">4,3</span></code>"
instead of "<code style="font-weight: bold;">3,4</code>".
The intent of this automatic resequencing is to speed up unification
processing if a repeat is requested (the Metamath Proof Engine is quite
strict about the order of hypotheses!)</li>
      </ul>
      <br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Ref</span><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Optional</li>
        <li><span style="font-weight: bold;">Ref</span> identifies the
Label of a theorem, axiom or logical hypothesis that justifies
derivation of the proof step's <span style="font-weight: bold;">Formula</span>
-- or may be a "<span style="font-weight: bold;">Local Ref</span>"
(e.g. "<code>#1</code>" or "<code>#syl.1</code>") as described below.<br>
        </li>
        <li><span style="font-weight: bold;">Ref</span>
is output by the Proof Assistant during Unification if it finds an
assertion in the database that justifies the proof step -- even if
there are unsatisfied Distinct Variable Restrictions associated with
the assertion (the Unification search continues even after a $d error,
looking for a unifying assertion that does not have a $d error, and if
no such assertion is found, a message is produced showing the
alterniative assertion choices.)<br>
        </li>
        <li><span style="font-weight: bold;">Ref</span>
may be input if the correct Label is known in advance, and/or if the
user wishes to override the output of Proof Assistant. <br>
        </li>
        <li>If <span style="font-weight: bold;">Ref</span> is input
and
one or more Hyps is omitted or = "?", and/or Formula is omitted, the
"Derive" feature
is invoked -- the input Ref is used to generate the missing Hyp and/or
Formula entries. (Derive operates on Derivation steps only, not on
Hypothesis steps.)<br>
        </li>
        <li>If <span style="font-weight: bold;">Ref</span> is present
in
the Proof Text when Unification is requested, the Proof Assistant will
attempt unification with the given <span style="font-weight: bold;">Ref</span>
first. Then, and only if&nbsp; the given <span
 style="font-weight: bold;">Ref</span>
is incorrect (invalid label, does not unify, etc.), will the algorithm
go through the tedious and perhaps horribly lengthy unification search
process
to find the correct Label.</li>
        <li>If <span style="font-weight: bold;">Ref</span> is input
but does not
unify correctly, the program produces a message showing alternative
assertions that do unify with the step.</li>
        <li>For a new theorem, the <code><span
 style="font-weight: bold;">Ref</span></code>s generated by Proof
Assistant for the theorem's logical hypotheses consist of the <code
 style="font-weight: bold;">THEOREM=</code> value suffixed with "<code><span
 style="font-weight: bold;">.1</span></code>", "<code
 style="font-weight: bold;">.2</code>", etc., in the order of the
appearance of the hypothesis Proof Steps.<br>
        </li>
        <li>Example: for new <code><span style="font-weight: bold;">THEOREM=XYZ</span></code>,
the Proof Assistant generates logical hypothesis Labels = <code
 style="font-weight: bold;">XYZ.1</code>, <code
 style="font-weight: bold;">XYZ.2</code>,
etc. for the Proof <span style="font-weight: bold;">Step</span>s
prefixed with "<code style="font-weight: bold;">h</code>", based on the
order of their appearance in the proof text area. If
this is unsatisfactory, input the desired Labels in the <code><span
 style="font-weight: bold;">Ref</span></code> fields to override the
default Ref values (for example "<code style="font-weight: bold;">maj</code>"
and "<code style="font-weight: bold;">min</code>" are the statement
labels in set.mm for <code style="font-weight: bold;">ax-mp</code> 's
logical hypotheses.)</li>
        <li>&nbsp;Note
that Labels on Logical Hypotheses must be unique within the Metamath
statement label namespace (no two statements can have the same Label).
In the event that the automatically generated Labels already exist in
the database -- highly unlikely -- an error message will be generated
and either the database should be modified or the Theorem's label
should be changed. Likewise if the user enters just some of the <span
 style="font-weight: bold;">Ref</span>'s and those conflict with the
database or other automatically generated Labels (moral of story is,
enter all of the <span style="font-weight: bold;">Refs</span> or none
of them ...)</li>
        <li>Note
also (!) that the order of logical hypotheses within a Metamath Theorem
is the order of their appearance within the database, which is not
necessarily the same as the order of their appearance within a proof.
The Proof Assistant, likewise, internally orders the hypotheses of new
theorems in the order of their appearance within the Proof Text area;
it does not alter the order of hypotheses for existing theorems. Either
way, this should have no impact on the RPN sequences of the proofs of
new theorems but <span style="text-decoration: underline;">those
contemplating future enhancements involving real-time updating might
want to pay attention: the order of logical hypotheses in a theorem's
frame affects the RPN sequences of proofs that <span
 style="font-style: italic;">refer to</span> the theorem in question</span>.</li>
        <li>"<span style="font-weight: bold;">Local Ref</span>" -- as a
text-editing short-cut for use by "advanced" users, a "Local Ref"
feature is provided. In the Ref field, enter "#" followed by the Ref or
Step of a previous proof step and press Ctrl-U (or other Unification
menu item). If there are no fields in error in the Proof Worksheet then
the proof step containing the Local Ref is deleted automatically and
any subsequent proof steps that refer to it as an hypothesis are
updated to point to the Local Ref'd step as the new hypothesis.&nbsp;
Note: A tutorial page has been added demonstrating the "<span
 style="font-weight: bold;">Local Ref</span>" feature. To use it, run
the&nbsp;&nbsp;&nbsp;&nbsp; <code>mmj2PaTutorial.bat</code> batch
command while in the <code>mmj2jar</code> directory. Then in the Proof
Assistant GUI, use the <code>File/Open Proof File</code> menu item to
open file <a href="../mmj2jar/PATutorial/PageLocalRef.mmp"><code>mmj2\mmj2jar\PATutorial\PageLocalRef.mmp</code></a>.<br>
        </li>
      </ul>
      <br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Formula</span><br>
      </td>
      <td style="vertical-align: top;">
      <ul>
        <li>Mandatory on Hypothesis Proof steps and the 'qed'
Derivation Proof Step.</li>
        <li>Optional if <span style="font-weight: bold;">Ref</span> is
entered on a non-'<code><span style="font-weight: bold;">qed</span></code>'
Derivation step -- Derive will attempt to generate the <span
 style="font-weight: bold;">Formula</span> from the <span
 style="font-weight: bold;">Ref</span> and <span
 style="font-weight: bold;">Hyp</span> input.<br>
        </li>
        <li><span style="font-weight: bold;">Formula</span> begins with
the first non-whitespace token following the <span
 style="font-weight: bold;">Step<code>:</code>Hyp<code>:</code>Ref</span>
string in a Proof Step statement, and continues until the next proof
text area statement begins.<br>
        </li>
        <li>The <code style="font-weight: bold;">Formula</code> must
begin with the Metamath file's designated <span
 style="font-weight: bold;">mmj2</span> "Provable Logic Statement Type"
(default = "<code style="font-weight: bold;">|-</code>", may be
overridden via a BatchMMJ2 RunParm).</li>
        <li><span style="font-weight: bold;">Formula</span> is
free-form and may be spaced or indented as the user desires, and may be
continued onto as many lines as needed of the proof text area.</li>
        <li>Unlike formulas in a Metamath .mm file, a Proof Step <span
 style="font-weight: bold;">Formula</span>
may not contain embedded comments (or non-whitespace symbols that are
not part of the formula!). Nor is the Formula terminated with "<code
 style="font-weight: bold;">$=</code>" or "<code
 style="font-weight: bold;">$.</code>". <br>
        </li>
        <li>The end of a Proof Step <span style="font-weight: bold;">Formula</span>
field is designated by the start of the next Proof Assistant text area
statement, not the Metamath "<code style="font-weight: bold;">$.</code>"
or "<code style="font-weight: bold;">$=</code>" tokens (which are not
used in the Proof Assistant GUI.)<br>
        </li>
        <li>The Proof Assistant GUI will not alter the spacing or
indentation of a user-input <span style="font-weight: bold;">Formula</span>
except when necessary for insertion of a <span
 style="font-weight: bold;">Ref&nbsp;</span> label in the <span
 style="font-weight: bold;">Proof Step</span> line -- or when Work
Variables are updated during unification, in which case the entire
formula is reformatted according to the current TMFF settings.<br>
        </li>
        <li>The <span style="font-weight: bold;">Formula</span> on a
hypothesis <span style="font-weight: bold;">Proof Step</span>
statement must be the exactly the same, symbol for symbol, as the
corresponding formula in the input
Metamath .mm file/database.&nbsp; Likewise with the formula on the "<code
 style="font-weight: bold;">qed</code>" <span
 style="font-weight: bold;">Proof Step</span>. (The easiest way to
accomplish this is with the <span style="font-weight: bold;">File/New</span>
menu item which preloads the hypotheses and "<code
 style="font-weight: bold;">qed</code>" <span
 style="font-weight: bold;">Proof Steps</span>.)</li>
        <li>Each Proof Step <span style="font-weight: bold;">Formula</span>
must be parseable using syntax axiom statements in the loaded Metamath
.mm file that are located prior to the theorem being proved or the <code
 style="font-weight: bold;">LOC_AFTER</code> location. Syntactic
analysis is performed as a necessary part of
validation/unification to construct a parse tree for the <span
 style="font-weight: bold;">Formula</span> (this should be obvious, but
be prepared in advance for ugly error messages coughed up by <span
 style="font-weight: bold;">mmj2</span>'s <span
 style="font-weight: bold;">Grammar</span>'s <span
 style="font-weight: bold;">Parser</span>! :)</li>
        <li>"Work Variables" may be generated by the Derive Feature,
and can be input by the user (except in the 'qed' and hypothesis
steps).&nbsp; The Work Variables represent unknown sub-expressions (or
variables) and have names corresponding to Type Code: "<code>&amp;W1</code>",
"<code>&amp;W2</code>", etc. for Type Code "<code>wff</code>"; "<code>&amp;C1</code>",
"<code>&amp;C2</code>", ... for Type Code "<code>class</code>", etc.
Refer to <code>\mmj2jar\AnnotatedRunParms.txt</code> for more
information -- (hint: search for "WorkVar" in the file.) Also, refer to
          <a href="StepUnifier.html">StepUnifier.html</a> and <a
 href="WorkVariables.html">WorkVariables.html</a>.<br>
        </li>
      </ul>
      <br>
      </td>
    </tr>
  </tbody>
</table>
<br>
<br>
<hr style="width: 100%; height: 2px;"><big><big><span
 style="font-weight: bold;"><a name="COMMENT_STATEMENT_TYPE"></a>COMMENT
Statement Type</span></big></big><br>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Comment:</span><br>
      <ul>
        <li>Identified by an Asterisk ("<code style="font-weight: bold;">*</code>")
character in column 1 of a line in the proof text area.</li>
        <li>A <span style="font-weight: bold;">Comment</span>
statement can continue onto multiple lines of the proof text&nbsp; area</li>
        <li>A
continuation line is identified by a space character in column 1 of a
line.</li>
        <li>Any valid Metamath tokens can be contained in a <span
 style="font-weight: bold;">Comment</span> statement except for&nbsp; "<code
 style="font-weight: bold;">$(</code>" or "<code
 style="font-weight: bold;">$)</code>"&nbsp; (<span
 style="font-style: italic;">Note:
the GUI itself does not validate the Comment contents, but Metamath.exe
and mmj2 do, so if a Proof Text containing embedded Metamath comments
is itself embedded as a comment in a Metamath file and input to these
programs, an error message will be generated and the problem will need
to be corrected before continuing.</span>)<br>
        </li>
      </ul>
      <br>
      </td>
    </tr>
  </tbody>
</table>
<br>
<span style="font-weight: bold;"></span><br>
<hr style="width: 100%; height: 2px;"><big><big><span
 style="font-weight: bold;"><a name="DISTINCT_VARIABLE_STATEMENT_TYPE"></a>DISTINCT
VARIABLE Statement Type</span></big></big><br>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Distinct
Variable:</span><br>
      <ul>
        <li>Identified by a "<code style="font-weight: bold;">$d</code>"
token in column 1.</li>
        <li>Must be a valid Metamath format <code
 style="font-weight: bold;">$d</code> but without the standard
terminator "<code style="font-weight: bold;">$.</code>", with no
embedded Metamath comments.</li>
        <li>May be located anywhere within the Proof Text area, applies
to the entire proof.</li>
        <li>More than one Distinct Variable Statement Type can be input
for a single proof.<br>
        </li>
        <li>The Distinct Variable restrictions specified are
accumulated with those already specified in the loaded Metamath .mm
database. Note: the new Set Soft Dj Vars Error Handling option on the
Edit Menu (and via RunParm) causes $d statements to be generated during
Unification, instead of reporting missing $d statements as errors.
Refer to <a href="../mmj2jar/AnnotatedRunParms.txt">mmj2\mmj2jar\AnnotatedRunParms.txt</a>
for additional information. <br>
        </li>
      </ul>
      </td>
    </tr>
  </tbody>
</table>
<br>
<span style="font-weight: bold;"><br>
</span><br>
<hr style="width: 100%; height: 2px;"><big><big><span
 style="font-weight: bold;"><a name="FOOTER_STATEMENT_TYPE"></a>FOOTER
Statement Type</span></big></big><br>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Footer:</span><br>
      <ul>
        <li>Identified by a "<code style="font-weight: bold;">$)</code>"
token in column 1 of the first line of the Proof Text area (by "token"
we mean that whitespace follows the "<code style="font-weight: bold;">$)</code>"
characters.)</li>
        <li>Any text following the "$)" token will be treated as an
error or ignored.<br>
        </li>
      </ul>
      </td>
    </tr>
  </tbody>
</table>
<br>
<br>
<hr style="width: 100%; height: 2px;"><big><big><span
 style="font-weight: bold;"><a name="GENERATED_PROOF_STATEMENT_TYPE"></a>GENERATED
PROOF Statement Type</span></big></big><br>
<br>
<table style="width: 75%; text-align: left;" border="5" cellpadding="2"
 cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Generated
Proof:</span><br>
      <ul>
        <li>Output by the Proof Assistant during Unification. Do not
input, will be erased!<br>
        </li>
        <li>Identified by a "<code style="font-weight: bold;">$=</code>"
token starting in column 1 of a Proof Text line (just before the
Footer).</li>
        <li>Consists of the Metamath RPN-format proof steps for the
theorem,
presented in columns 6 thru 79 of proof text lines (defaults may be
adjusted using RunParms), and continued onto as
many lines as needed, and followed by a "<code
 style="font-weight: bold;">$.</code>" token.</li>
      </ul>
      </td>
    </tr>
  </tbody>
</table>
<br>
<br>
<hr style="width: 100%; height: 2px;"><span style="font-weight: bold;"><br>
</span>
</body>
</html>
